Reliable Software in the LLM Era

https://quint.sh/posts/llm_era

Gabriela Moreira(Informal Systems)による、LLM時代にソフトウェアの信頼性をどう確保するかについての論考と実例報告

2025年11月17日公開、2026年4月9日更新

問題意識

LLMはコード生成を変えた一方で、新しいフラストレーションも生んでいる

巨大なAI生成のdiffを見て正しいか分からない、それっぽく動くが微妙に間違ったコード、通っているが何もテストしていないテスト、といった経験

LLMの本質は「正しく見えるテキストを作ること」、だからこそ検証が難しい

AIは過信する、現実との照合が必要

Quintの位置付け

Quintは英語とコードの中間に座る理想的な検証ポイント

コードより抽象的で人間が推論しやすく、英語と違って実行可能・機械的検証が可能

シミュレータ・モデルチェッカ・REPLによって探索とプロパティ検査で確信を積み上げられる

モデルベーステストによって仕様と実装を決定論的に接続でき、仕様レベルの確信をコードレベルへ持ち越せる

検証ユースケース: Malachite

MalachiteはTendermint系の本番品質BFT合意エンジン

Circle(USDC発行元)に買収され、新しいブロックチェーンArcの基盤になっている

Malachiteのプロトコル設計は最初からQuintで行われていた

Tendermintに複数の最適化が入っており、コンセンサスコアだけで4コンポーネント

今回の変更内容

通常のTendermint(3F+1耐性)からFast Tendermintへの切替

Fast Tendermintは5F+1ノードでFビザンチンノードに耐える代わりに通信1ステップ削減

従来の見積もり: 数ヶ月

今回の挑戦: Quint+AIで1週間で完了させる、実際に成功した

出発点

既存TendermintQuint仕様(Choreo フレームワーク使用)を持っていた

TendermintはInformal Systemsが好んでモデル化するプロトコルで複数バージョンの仕様あり

設計者Manuによる英語の新プロトコル記述・草稿証明・論文も用意

プロトコル設計は人間がやり、AIには任せない方針

AIは「設計者」ではなく「翻訳者」として使う

4ステップワークフロー

Spec Change: 既存Quint仕様 + 英語記述を入力にAIが新仕様を生成、quint parse・quint typecheckで即フィードバックループ

Spec Validation: 人間が最も時間を割くべき段階、AIがシナリオを提案し人間がドメイン知識でプロパティや到達可能性を質問する

Code Change: 旧仕様・新仕様・両者のdiffをAIに渡して実装を生成、曖昧な自然言語ではなく形式モデルを翻訳元に使う

Code Validation: モデルベーステストで仕様のシナリオを実装に再生し挙動一致をアサート、CIに乗るテストスイートとして恒常化する

Spec Validationで見つけたもの

再ブロードキャスト機構: トリガできるか、受信して反応できるか

代替決定伝搬: 通常フローではなくこちらが起きるシナリオを発見・文書化

ビザンチン耐性の前提: わざと耐性超過のビザンチンノードを置いた版で「合意不一致が発生し得るか」を確認、発生しないなら前提が非現実的

結果: Manuの英語仕様の小さなバグ2件を1日午後で発見

Code Validationの先

トレース検証(trace validation)を進めている

テスト環境・テストネット・本番から取得した実トレースが仕様に準拠しているかを検証する

「実装が仕様通りに振る舞いうる」だけでなく「実際にそう振る舞っている」を確認するループの閉じ方

結果の数字

仕様修正と検証: 約2日

コード生成とテスト(精緻化・デバッグ含む): 約1週間

従来の数ヶ月見積もりに対して大幅短縮

副次的な利点: 仕様がデバッグの羅針盤になる

AIがログを読んで「YのときにXをブロードキャストすべき」と判断

AIがQuint仕様を読み「いや、仕様ではYでXをブロードキャストしないのが正、設計上の挙動」と訂正

結果: 別の仮説に即座に移れる

英語仕様だと「文書化漏れかも」「不完全かも」と疑い続ける必要がある

検証済みQuint仕様なら、必要であれば検証段階で露見しているはず、と確信を持って排除できる

人間とAIの両方が間違った疑いに引きずり込まれにくくなる

結論

実行可能仕様こそLLM支援開発の理想的検証ポイント

英語とコードの中間にあり、人間の推論にも機械的検証にも適する

AIの過信に対抗するのは、より多くのAIではなく、より良い検証ツール

Quintは人間が複雑系を推論する道具として作られたが、AIにQuintを与えるとAIをガードレールできる

LLMは翻訳に長け、Quintの決定論的ツールが推論を担う、という分業

仕事は「コードを書くこと」から「AI生成コードを検証すること」へ、「正しいとは何かを定義すること」が極めて重要になる